COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Summary of Changes to Theorem Prover files for SAIL version
C00010 00003	Fixes to xxxs.lis
C00011 ENDMK
C⊗;
Summary of Changes to Theorem Prover files for SAIL version

Here it is.  I will verify it next time I import a new version
and keep you informed.  At SAIL

        (status features sail) -> T 

if you want to add some more conditional stuff to the sources.


--------------------------   the  changes   ---------------------------

(1) to COMPLR.INI
1.1 omit  
        (PUTPROP (QUOTE LISP) (QUOTE (PS MACLISP)) (QUOTE PPN))
;;  The SAIL compiler and lisp seem to know where to look for system things

1.2 add the following to make BCOMPLR forget its notion of MATCH-MACRO
        (REMPROP 'MATCH-MACRO 'AUTOLOAD)
        (REMPROP 'MATCH-MACRO 'MACRO)
;; in bcomplr 
        (plist 'match-macro) -> 
        (MACRO |MATCH-MACRO MACRO| AUTOLOAD (MACROD FAS DSK (MAC LSP))) 
;; which clashes with use of MATCH-MACRO in  MATCH defined in BASIS


(2) to LISP.INI
2.1  omit the PPN putprops
        (PUTPROP (QUOTE LISP) (QUOTE (PS MACLISP)) (QUOTE PPN))
        (PUTPROP (QUOTE THM) (QUOTE (AUX |CL.THM|)) (QUOTE PPN))
 change
        (PUTPROP (QUOTE  MAKE-THM) (QUOTE  ((THM) MAKE-THM FASL)) (QUOTE  AUTOLOAD))
to
        (PUTPROP (QUOTE  MAKE-THM) (QUOTE  (MAKETH FAS)) (QUOTE  AUTOLOAD))
2.2 omit the display hacking,debugging and editing stuff
	(SSTATUS LINMODE T)
	(SETQ DEFAULTF (QUOTE ((*) FOO LSP)))
	(FASLOAD FIXIT FASL LISP)
	(PROG (FASLOAD) (FASLOAD UCEDIT FASL LISP))
	(DEFUN TYPE FEXPR (X)
	  (PRINC (QUOTE |Type this file:  |) T)
	  (PRIN1 X T)
	  (TERPRI T))
	(FASLOAD TOPS-20-EMACS-TO-THM FASL THM)

2.3 add directory default Gc-demon and E-Maclisp interface stuff

(PROGN
  (APPLY 'CRUNIT (LIST 'DSK (STATUS UDIR)))
  (HELP)
  (fasload demon fas dsk (mac lsp))
  (fasload file fas dsk (aid lsp))
  (setq em:no-init t)
  (fasload emaclsp fas dsk (mac lsp))
  (COND ((STATUS NOFEATURES NEWIO)
         (FASLOAD ESCI FAS DSK (MAC LSP))))
  (ESCI-ENB)

)



(3) to MAKE-THM.LISP
(3.1) fix file loading format - omit (QUOTE THM) as device,  PS replaced by DSK
change 
        (LOOP FOR ROOT IN (QUOTE (BASIS GENFACT EVENTS CODE-1-A CODE-B-D CODE-E-M
    			          CODE-N-R CODE-S-Z IO PPR))
    	      DO (APPLY (FUNCTION FASLOAD) (LIST ROOT (QUOTE FASL) (QUOTE THM))))
to
    (LOOP FOR ROOT IN (QUOTE (BASIS GENFACT EVENTS CODE-1-A CODE-B-D CODE-E-M
			      CODE-N-R CODE-S-Z IO PPR))
	  DO (APPLY (FUNCTION FASLOAD) (LIST ROOT (QUOTE FASL) )))
;; seems to truncate FASL to FAS without complaint
change
       (LET ((TEMP (PROBEF (LIST (LIST (QUOTE PS) (STATUS HOMEDIR))
   			      (QUOTE THM) (QUOTE INI)))))
         (COND (TEMP (LOAD TEMP))))
to
    (LET ((TEMP (PROBEF (LIST (LIST (QUOTE DSK) (STATUS HOMEDIR))
			      (QUOTE THM) (QUOTE INI)))))
      (COND (TEMP (LOAD TEMP))))

;; I believe the looking for the maclisp directory stuff
;; can be omitted since here maclisp seems to know where to look
;; and it is a noop at SAIL

(3.2) add code to setup E-Maclisp interface and fix file defaults

    (COND ((AND (STATUS FEATURES SAIL) SI:ECALLEDP)
	   (SETQ -EM:HERALD- ())
	   (EM:MAIL-INTERFACE-INITIALIZE)))

   (APPLY 'CRUNIT (LIST 'DSK (STATUS UDIR)))

;; to the  MAKE- function somewhere after the (SUSPEND)
;; Then the [prg,ppn] will default to the users current area.
;; This seems to be adequate for the ordinary user.  
;; For fancier things the user can always hack the defaults as desired.




(4) to BASIS  
(4.1) to get around SAIL i/o bug modify definition of  NOTE-LIB 
at the end of replace
        (SETQ LIB-FILE FILE)
        (OPEN LIB-FILE (QUOTE IN)) 
by
        (SETQ LIB-FILE (OPEN FILE1 (QUOTE IN)) )


Fixes to xxxs.lis

(SWAPOUT "PROVEALL-TEMP") becomes the two events 
(MAKE-LIB "PROVEALL-TEMP") 
(NOTE-LIB "PROVEALL-TEMP.LIB" "PROVEALL-TEMP.LISP")